feat(syntax): regions_introduced_by helper — Phase 3b scaffolding (#225) by hyperpolymath · Pull Request #230 · hyperpolymath/ephapax

hyperpolymath · 2026-05-30T14:23:00Z

Summary

Adds `regions_introduced_by : expr -> list region_name`, a `Fixpoint` collecting region names introduced by `ERegion` subterms.

This is scaffolding infrastructure for Phase D slice 4 Phase 3b (`subst_typing_gen_l1_m_tfuneff`) per ephapax issue #225's recommended option (a).

Why now

Phase 3b's main obstacle (per #225 analysis): retyping a TFunEff value at `r :: R` (post T_Region_L1 inside substituee body) requires `r ∈ R_in_v`, but `r` is fresh and unconstrained relative to `R_in_v`. Option (a) resolves this by adding a syntactic over-approximation precondition:

```coq
(forall r, In r (regions_introduced_by e) -> In r R_in_v)
```

The precondition is decomposable through compound rules (each sub-expression's `regions_introduced_by` is a subset of the parent's) and discharges directly at the `T_Region_L1` case (where `r` is the head of `regions_introduced_by (ERegion r e')`).

Why split this scaffold off

The full Phase 3b lemma is ~400 lines mirroring Phase 2 with `shift_typing_gen_l1_m` threading at every binder-descent case (Phase 2's `ground_nonlinear_value_shift_id_l1` shortcut doesn't apply to non-scalar TFunEff lambdas — `shift c 1 (ELam T0 e0) = ELam T0 (shift (S c) 1 e0)`, which changes the body's de Bruijn indices). That scope exceeds the single-session budget that Phase 1 / Phase 2 / Phase 3a have been shipping at.

Landing the helper alone keeps a future Phase 3b implementation PR focused on the lemma body without re-introducing the predicate.

Verification

```
$ cd /tmp/ephapax-phase-3b/formal && just all
coq_makefile -f _CoqProject -o build.mk
make -f build.mk
COQDEP VFILES
COQC Syntax.v
COQC Typing.v
COQC Modality.v
COQC TypingL1.v
COQC Semantics.v
COQC Semantics_L1.v
COQC Counterexample.v
COQC Echo.v
COQC TypingL2.v
COQC L4.v
(exit 0)
```

Rocq 9.1.1 / Coq 8.18. Zero new admits, zero new axioms. Helper is currently unused by any lemma — landing as preparatory infrastructure.

Owner-directive compliance

✅ Does NOT modify `Semantics.v`.
✅ Does NOT add new admits or axioms.
✅ Pure syntactic Fixpoint; no semantic consequences.
✅ Lives in `Syntax.v` alongside `is_ground_nonlinear_ty` and `is_tfuneff_ty` (matching precedent).

Refs

ephapax#225 — Phase 3b tracking issue, option (a)
formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3b
PR feat(L1): Phase D slice 4 Phase 2 — subst_typing_gen_l1_m_ground_nonlinear + helpers #220 — Phase 2 (`subst_typing_gen_l1_m_ground_nonlinear`) for structural template
PR feat(L2): Phase D slice 4 Phase 4a — preservation_l2_app_eff_beta_linear + hotfix duplicate tfuneff_lambda_retype_l1_m #228 — Phase 4a (`preservation_l2_app_eff_beta_linear`) for Phase 4 use shape

🤖 Generated with Claude Code

… TFunEff substitution Adds `regions_introduced_by : expr -> list region_name`, a fixpoint collecting region names introduced by `ERegion` subterms of an expression. This is scaffolding infrastructure for Phase D slice 4 Phase 3b (`subst_typing_gen_l1_m_tfuneff`) per ephapax issue #225's recommended option (a). The helper is the precondition shape that allows Phase 3b to discharge `T_Region_L1` cases inside the substituee body — when the body introduces a region `r`, retyping a TFunEff value at the extended `r :: R` requires `r ∈ R_in_v`, which is supplied via `(forall r, In r (regions_introduced_by e) -> In r R_in_v)`. The full Phase 3b lemma (~400 lines mirroring Phase 2 with `shift_typing_gen_l1_m` threading for binder-descent cases) exceeds single-session scope and remains tracked at issue #225. This PR ships only the helper so downstream Phase 3b drafts can reference it without re-introducing the predicate. Build oracle: `just -f formal/Justfile all` green (Rocq 9.1.1 / Coq 8.18). Zero new admits, zero new axioms. Helper is currently unused by any lemma — landing as preparatory infrastructure to keep Phase 3b's eventual implementation diff focused on the lemma body. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-05-30T14:23:53Z

🔍 Hypatia Security Scan

Findings: 74 issues detected

Severity	Count
🔴 Critical	13
🟠 High	13
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in abi-verify.yml",
    "type": "unknown",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "unknown",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…rexample for TFunEff β (#234) ## Summary Ships a **mechanised proof** that preservation_l2 fails for TFunEff substituends inside fresh-region scopes, plus a design-doc addendum prescribing the conditional Phase 4c closure path. This is the L1/L2 analogue of \`formal/Counterexample.v\` (which witnesses the legacy preservation's soundness gap), providing rigorous justification for the **conditional** preservation_l2 statement that Phase 4c will ship. ## What this PR ships ### \`formal/Counterexample_L2.v\` (new) Three Qed lemmas (**zero axioms, zero admits**) witnessing the soundness gap: - \`e_before_typed\` — input \`EApp outer v2\` types via T_App_L2_Eff at \`TFunEff TUnit TUnit [] []\`. - \`e_step\` — operational step S_App_Fun reduces to \`ERegion r2 v2\`. - \`e_after_untypable\` — no L1 derivation exists for the β-result at the same outer type. **Configuration:** \`\`\`coq T1_inner = TFunEff TUnit TUnit [] [] (* R_in_v = [] *) outer = ELam T1_inner (ERegion r2 (EVar 0)) (* body introduces fresh r2 *) v2 = ELam TUnit EUnit (* a value of type T1_inner *) e_before = EApp outer v2 (* well-typed *) e_after = ERegion r2 v2 (* β-result, NOT well-typed *) \`\`\` **Structural mechanism:** T_Region_L1's \`~ In r (free_regions T)\` premise prevents the fresh r from being in \`R_in_v ⊆ free_regions(TFunEff)\`, so the post-β term's inner TFunEff value cannot re-type at the new threaded R = \`r :: R\`. ### \`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md\` addendum New §"Phase 4c addendum (2026-05-30) — conditional preservation_l2 for TFunEff β" documents the counterexample and prescribes three resolution paths: 1. **Conditional preservation_l2 (recommended)** — Phase 3b lemma takes the \`regions_introduced_by(e) ⊆ R_in_v\` precondition; Phase 4c β-case requires it; programs outside form a documented soundness-gap class. Aligns with the \`Counterexample.v\` precedent for legacy preservation. 2. **Region-polymorphic TFunEff** — type-system change deferred to a future redesign. 3. **L2 region-transfer combinator** — adds L2 expressiveness in a future PR. ### \`formal/_CoqProject\` Adds \`Counterexample_L2.v\` after \`TypingL2.v\` in the build order. ### \`.machine_readable/6a2/STATE.a2ml\` \`next_action\` shifted to Phase 3b implementation (option-(a) precondition codified by this PR's counterexample); \`last_action\` records the counterexample landing. ## Build + assumption audit - \`coqc -R . Ephapax\` clean rebuild across all 11 .v files. - \`Print Assumptions e_before_typed\` / \`e_step\` / \`e_after_untypable\` → "Closed under the global context" for all three. **Zero axioms, zero admits.** ## Owner-directive compliance (CLAUDE.md 2026-05-27) - ✅ Does not modify \`formal/Semantics.v\` or \`formal/Counterexample.v\` (the legacy soundness-gap artifacts). - ✅ Does not patch \`formal/Typing.v\` (legacy judgment). - ✅ Does not close any residual \`formal/Semantics_L1.v\` admit. - ✅ Adds NEW infrastructure (a new file) orthogonal to legacy admits, mirroring the precedent of \`Counterexample.v\` for the legacy preservation. - ✅ No new \`Axiom\` or \`Admitted\` markers. ## Why this matters Before Phase 3b implementation (~400 lines per PR #230's analysis), this counterexample **mechanically witnesses** the structural constraint the lemma must satisfy. The conditional preservation_l2 design is now rigorously justified rather than asserted on paper. ## Test plan - [x] \`coqc -R . Ephapax\` rebuild across all 11 .v files, zero errors / warnings. - [x] \`Print Assumptions\` audit shows zero axioms on all three counterexample lemmas. - [x] Configuration in \`Counterexample_L2.v\` matches the on-paper analysis in #225 comment 4583148707. - [x] First PR to be gated by the new CI Coq build oracle from PR #231. ## Refs - ephapax#225 — Phase 3b tracking issue (option (a) selected). - ephapax#225 comment 4583148707 — on-paper prototype that motivated this mechanical formalisation. - PR #230 — \`regions_introduced_by\` scaffold (option (a)'s syntactic helper). - PR #228 — Phase 4a (linear T1, no soundness gap). - PR #233 — Phase 4b (ground-non-linear T1, no soundness gap). - PR #231 — CI Coq build oracle (this PR is its first beneficiary). - \`formal/Counterexample.v\` — legacy preservation counterexample (precedent for this file's structure). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…DE.md DO #4 (closes nothing, files #235) Pre-implementation review of Phase 3b's option (a) precondition (forall r, In r (regions_introduced_by e) -> In r R_in_v) found it INSUFFICIENT to discharge T_Lam_L1_*_Eff body cases of the planned subst_typing_gen_l1_m_tfuneff lemma. Why: the substitution lemma recurses into inner lambda bodies (Phase 2 does so via the IH at formal/Semantics_L1.v:1929-1942). Inner T_Lam_L1_*_Eff bodies type at the lambda's declared R_in_inner. R_in is type-level — it lives in the TFunEff slot of the function's TYPE, not in syntax. `regions_introduced_by(e)` only collects ERegion subterms' first arguments; R_in_inner is invisible to it. `tfuneff_lambda_retype_l1_m` (PR #224) requires R' ⊆ R_in_v to discharge T_Lam_L1_*_Eff's side condition. We have no way to bound inner R_in by R_in_v. Phase 2's `subst_typing_gen_l1_m_ground_nonlinear` dodges this via `ground_nonlinear_retype_l1_m`, which is fully (m, R, G)-polymorphic. Phase 3b's TFunEff retype has no analogous escape. Three resolution options documented: 1. Syntactic helper `declared_lambda_r_ins` — requires ELam annotation extension (parameter type only in current syntax). 2. Semantic precondition over the derivation — clean meaning, awkward in Coq. 3. Leaf-only Phase 3b via `tfuneff_lambda_free e` predicate — tactical landing; Phase 5 compound-value redesign subsumes (1)/(2) at leisure. Recommended: option (3). Owner decision required before Phase 3b implementation can start. This PR contains documentation only: - formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md gains a Phase 3b addendum documenting the gap and three resolution options. - .machine_readable/6a2/STATE.a2ml flips phase to `blocked-on-owner-decision` with next_action pointing at #235. No formal/*.v changes. Predecessor PRs unaffected: - Phase 4a (#228) MERGED. - Phase 4b (parallel session, #233) MERGED. - Phase 4c counterexample (#234) auto-merge pending. Phase 4c's `Counterexample_L2.v` independently justifies the conditional preservation_l2 statement regardless of which Phase 3b resolution lands. Per CLAUDE.md owner directive §DO #4 (escalate before patching): this PR IS the escalation. Owner-directive compliance: - No Semantics.v / Typing.v / Counterexample.v touch - No new Axiom / Admitted markers - No closure of residual Semantics_L1.v admits - No sibling-region-disjointness side conditions - No proposal to close `Theorem preservation` to Qed. Refs: #225 (Phase 3b parking lot), #230 (regions_introduced_by helper), #233 (Phase 4b), #234 (Phase 4c counterexample), Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

/ #242) (#237) ## Summary Phase D slice 4 Phase 3b — design-gap finding (#235) **+ 4-stage staged resolution plan** owner-approved 2026-05-30 PM. Stages tracked at #239 / #240 / #241 / #242. No `formal/*.v` changes. No CI changes (the parallel-session PR #236 owns the Coq EACCES fix). ## 4-stage staged resolution plan The original three-option framing in #235 is **superseded** by a staged plan that captures all three "Interesting" values without committing to any single option's downsides. | Stage | Issue | Scope | Captures value of | |---|---|---|---| | **Stage 1 — IMMEDIATE** | #239 | Leaf-only Phase 3b via `tfuneff_lambda_free` + `Counterexample_L2_nested.v` + 2-condition `preservation_l2`. | Option (3) — principled deferral, honest 2-condition statement. | | **Stage 2 — parallel L4 track** | #240 | `ELam T_param R_in R_out body` annotation extension. AST + typing rule + cascading. | Option (1) — L4 "type-level → program-level commitments". | | **Stage 3 — post-Stage-2** | #241 | Relaxed Phase 3b via `declared_lambda_r_ins ⊆ R_in_v` + CPS v-typing argument. Nested-condition collapses. | Option (2) — higher-order proof style enters codebase. | | **Stage 4 — Phase 5** | #242 | Compound non-linear + region-substitution machinery + **unconditional** `preservation_l2`. | The final destination. | ### Why staging beats single-option commitments - **(1) alone**: forces AST migration before unblocking preservation_l2. - **(2) alone**: introduces inductive-over-derivations predicate with no other use in the codebase. - **(3) alone**: ends with conditional preservation_l2 forever (no path to unconditional). The staged plan: (3) ships today's value at Stage 1, (1) lands L4's value at L4's timeline (Stage 2), (2)'s value is harvested at exactly the point CPS is necessary not over-engineered (Stage 3), (4) reaches unconditional preservation_l2 as the natural sum. ### Stage 1's correctness is delivered, not provisional Each of the 2 conditions on Stage 1's `preservation_l2` has a **mechanised counterexample**: - `Counterexample_L2.v` (already on main, PR #234) — fresh-region gap. - `Counterexample_L2_nested.v` (new in Stage 1) — nested-lambda gap. Programs outside the conditional form a precisely-documented soundness class. ### Sequencing - Stage 1 green-lit (#239). Implementation ships next session. - Stages 2-4 tracked but NOT actioned this session. - Stage 3 blocked on Stage 2; Stage 4 blocked on Stage 3; Stage 2 independent of Stage 1. ## Changes - `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` — Phase 3b addendum (gap finding + 3-options framing) **+ Phase 3b resolution addendum (4-stage staged plan)**. - `.machine_readable/6a2/STATE.a2ml` — phase = `implementation`; next_action = Stage 1 (#239) implementation. No `formal/*.v` changes; Coqc 8.18.0 unaffected. ## Predecessor PRs - Phase 4a (#228) MERGED — `preservation_l2_app_eff_beta_linear`. - Phase 4b (#233) MERGED — `preservation_l2_app_eff_beta_ground_nonlinear_l1`. - Phase 4c (#234) MERGED — `Counterexample_L2.v` 3-Qed soundness-gap witness. ## Owner-directive compliance (across all 4 stages) - ✅ No `Semantics.v` / `Typing.v` / `Counterexample.v` (legacy) touch. - ✅ No new `Axiom` / `Admitted` markers. - ✅ No closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure under the four-layer redesign. - ✅ Per-layer derivation: preservation_l2 closes via L2 infra; legacy preservation remains Admitted (PROVABLY FALSE) per 2026-05-27 directive. ## Test plan - [ ] CI green (no code changes; Coq oracle should pass unchanged — pending PR #236's EACCES fix landing). - [ ] Issues #235 / #239 / #240 / #241 / #242 cross-referenced. Refs: #225 (Phase 3b parking lot), #230 (`regions_introduced_by`), #233 (Phase 4b), #234 (Phase 4c), #235 (parent finding), #236 (parallel Coq EACCES fix), #239 (Stage 1), #240 (Stage 2), #241 (Stage 3), #242 (Stage 4). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath enabled auto-merge (squash) May 30, 2026 14:23

hyperpolymath merged commit df6d7b5 into main May 30, 2026
17 checks passed

hyperpolymath deleted the phase-d-slice-4-phase-3b-tfuneff-subst-2026-05-30 branch May 30, 2026 14:23

This was referenced May 30, 2026

Phase D slice 4 Phase 3b — TFunEff substitution-lemma extension (deferred from #224) #225

Closed

docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234

Merged

This was referenced May 30, 2026

Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases #235

Closed

docs: Phase 3b 4-stage staged resolution plan (#235 → #239 / #240 / #241 / #242) #237

Merged

hyperpolymath mentioned this pull request May 30, 2026

Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(syntax): regions_introduced_by helper — Phase 3b scaffolding (#225)#230

feat(syntax): regions_introduced_by helper — Phase 3b scaffolding (#225)#230
hyperpolymath merged 1 commit into
mainfrom
phase-d-slice-4-phase-3b-tfuneff-subst-2026-05-30

hyperpolymath commented May 30, 2026

Uh oh!

github-actions Bot commented May 30, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented May 30, 2026

Summary

Why now

Why split this scaffold off

Verification

Owner-directive compliance

Refs

Uh oh!

github-actions Bot commented May 30, 2026

🔍 Hypatia Security Scan

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant